Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(app(ack,0),y)	→ app(succ,y)
2:	app(app(ack,app(succ,x)),y)	→ app(app(ack,x),app(succ,0))
3:	app(app(ack,app(succ,x)),app(succ,y))	→ app(app(ack,x),app(app(ack,app(succ,x)),y))

There are 7 dependency pairs:


4:	APP(app(ack,0),y)	→ APP(succ,y)
5:	APP(app(ack,app(succ,x)),y)	→ APP(app(ack,x),app(succ,0))
6:	APP(app(ack,app(succ,x)),y)	→ APP(ack,x)
7:	APP(app(ack,app(succ,x)),y)	→ APP(succ,0)
8:	APP(app(ack,app(succ,x)),app(succ,y))	→ APP(app(ack,x),app(app(ack,app(succ,x)),y))
9:	APP(app(ack,app(succ,x)),app(succ,y))	→ APP(ack,x)
10:	APP(app(ack,app(succ,x)),app(succ,y))	→ APP(app(ack,app(succ,x)),y)

The approximated dependency graph contains one SCC: {5,8,10}.

Consider the SCC {5,8,10}. By taking the AF π with π(APP) = 1 together with the lexicographic path order with precedence ack ≻ 0, ack ≻ app and ack ≻ succ, rule 10 is weakly decreasing and the rules in {1-3,5,8} are strictly decreasing. There is one new SCC.
- Consider the SCC {10}. By taking the AF π with π(APP) = 2 together with the lexicographic path order with precedence ack ≻ 0, ack ≻ app and ack ≻ succ, the rules in {1-3,10} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.09 seconds) --- May 3, 2006